<!DOCTYPE html>
<html lang="zh-CN">
<head>
  <meta charset="UTF-8">
<meta name="viewport" content="width=device-width">
<meta name="theme-color" content="#222"><meta name="generator" content="Hexo 6.3.0">

  <link rel="apple-touch-icon" sizes="180x180" href="/blog/images/apple-touch-icon-next.png">
  <link rel="icon" type="image/png" sizes="32x32" href="/blog/images/Horse.png">
  <link rel="icon" type="image/png" sizes="16x16" href="/blog/images/Horse.png">
  <link rel="mask-icon" href="/blog/images/logo.svg" color="#222">

<link rel="stylesheet" href="/blog/css/main.css">



<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.4.0/css/all.min.css" integrity="sha256-HtsXJanqjKTc8vVQjO4YMhiqFoXkfBsjBWcX91T1jr8=" crossorigin="anonymous">
  <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/fancybox/3.5.7/jquery.fancybox.min.css" integrity="sha256-Vzbj7sDDS/woiFS3uNKo8eIuni59rjyNGtXfstRzStA=" crossorigin="anonymous">

<script class="next-config" data-name="main" type="application/json">{"hostname":"yanlwsometing.gitee.io","root":"/blog/","images":"/blog/images","scheme":"Pisces","darkmode":false,"version":"8.16.0","exturl":false,"sidebar":{"position":"left","display":"post","padding":18,"offset":12},"copycode":{"enable":true,"show_result":true,"style":"flat"},"bookmark":{"enable":false,"color":"#222","save":"auto"},"mediumzoom":false,"lazyload":false,"pangu":false,"comments":{"style":"tabs","active":null,"storage":true,"lazyload":false,"nav":null},"stickytabs":false,"motion":{"enable":false,"async":false,"transition":{"menu_item":"fadeInDown","post_block":"fadeIn","post_header":"fadeInDown","post_body":"fadeInDown","coll_header":"fadeInLeft","sidebar":"fadeInUp"}},"prism":false,"i18n":{"placeholder":"搜索...","empty":"没有找到任何搜索结果：${query}","hits_time":"找到 ${hits} 个搜索结果（用时 ${time} 毫秒）","hits":"找到 ${hits} 个搜索结果"}}</script><script src="/blog/js/config.js"></script>

    <meta name="description" content="穷则独善其身，达则兼济天下！">
<meta property="og:type" content="website">
<meta property="og:title" content="yanlwsometing">
<meta property="og:url" content="https://yanlwsometing.gitee.io/blog/index.html">
<meta property="og:site_name" content="yanlwsometing">
<meta property="og:description" content="穷则独善其身，达则兼济天下！">
<meta property="og:locale" content="zh_CN">
<meta property="article:author" content="yanlw">
<meta property="article:tag" content="博客">
<meta name="twitter:card" content="summary">


<link rel="canonical" href="https://yanlwsometing.gitee.io/blog/">



<script class="next-config" data-name="page" type="application/json">{"sidebar":"","isHome":true,"isPost":false,"lang":"zh-CN","comments":"","permalink":"","path":"index.html","title":""}</script>

<script class="next-config" data-name="calendar" type="application/json">""</script>
<title>yanlwsometing</title>
  








  <noscript>
    <link rel="stylesheet" href="/blog/css/noscript.css">
  </noscript>
</head>

<body itemscope itemtype="http://schema.org/WebPage">
  <div class="headband"></div>

  <main class="main">
    <div class="column">
      <header class="header" itemscope itemtype="http://schema.org/WPHeader"><div class="site-brand-container">
  <div class="site-nav-toggle">
    <div class="toggle" aria-label="切换导航栏" role="button">
        <span class="toggle-line"></span>
        <span class="toggle-line"></span>
        <span class="toggle-line"></span>
    </div>
  </div>

  <div class="site-meta">

    <a href="/blog/" class="brand" rel="start">
      <i class="logo-line"></i>
      <h1 class="site-title">yanlwsometing</h1>
      <i class="logo-line"></i>
    </a>
  </div>

  <div class="site-nav-right">
    <div class="toggle popup-trigger" aria-label="搜索" role="button">
    </div>
  </div>
</div>



<nav class="site-nav">
  <ul class="main-menu menu"><li class="menu-item menu-item-home"><a href="/blog/" rel="section"><i class="fa fa-home fa-fw"></i>首页</a></li><li class="menu-item menu-item-tags"><a href="/blog/tags/" rel="section"><i class="fa fa-tags fa-fw"></i>标签</a></li><li class="menu-item menu-item-categories"><a href="/blog/categories/" rel="section"><i class="fa fa-th fa-fw"></i>分类</a></li><li class="menu-item menu-item-archives"><a href="/blog/archives/" rel="section"><i class="fa fa-archive fa-fw"></i>归档</a></li><li class="menu-item menu-item-commonweal"><a href="/blog/404/" rel="section"><i class="fa fa-heartbeat fa-fw"></i>公益 404</a></li>
  </ul>
</nav>




</header>
        
  
  <aside class="sidebar">

    <div class="sidebar-inner sidebar-overview-active">
      <ul class="sidebar-nav">
        <li class="sidebar-nav-toc">
          文章目录
        </li>
        <li class="sidebar-nav-overview">
          站点概览
        </li>
      </ul>

      <div class="sidebar-panel-container">
        <!--noindex-->
        <div class="post-toc-wrap sidebar-panel">
        </div>
        <!--/noindex-->

        <div class="site-overview-wrap sidebar-panel">
          <div class="site-author animated" itemprop="author" itemscope itemtype="http://schema.org/Person">
    <img class="site-author-image" itemprop="image" alt="yanlw"
      src="/blog/images/avatar.jpg">
  <p class="site-author-name" itemprop="name">yanlw</p>
  <div class="site-description" itemprop="description">穷则独善其身，达则兼济天下！</div>
</div>
<div class="site-state-wrap animated">
  <nav class="site-state">
      <div class="site-state-item site-state-posts">
        <a href="/blog/archives/">
          <span class="site-state-item-count">23</span>
          <span class="site-state-item-name">日志</span>
        </a>
      </div>
      <div class="site-state-item site-state-categories">
          <a href="/blog/categories/">
        <span class="site-state-item-count">9</span>
        <span class="site-state-item-name">分类</span></a>
      </div>
      <div class="site-state-item site-state-tags">
          <a href="/blog/tags/">
        <span class="site-state-item-count">18</span>
        <span class="site-state-item-name">标签</span></a>
      </div>
  </nav>
</div>
  <div class="links-of-author animated">
      <span class="links-of-author-item">
        <a href="https://gitee.com/yanlwsometing" title="Gitee → https:&#x2F;&#x2F;gitee.com&#x2F;yanlwsometing" rel="noopener me" target="_blank"><i class="fab fa-gitee fa-fw"></i>Gitee</a>
      </span>
      <span class="links-of-author-item">
        <a href="mailto:1977712019@qq.com" title="Mail → mailto:1977712019@qq.com" rel="noopener me" target="_blank"><i class="fa fa-envelope fa-fw"></i>Mail</a>
      </span>
      <span class="links-of-author-item">
        <a href="https://weibo.com/" title="Weibo → https:&#x2F;&#x2F;weibo.com&#x2F;" rel="noopener me" target="_blank"><i class="fab fa-weibo fa-fw"></i>Weibo</a>
      </span>
      <span class="links-of-author-item">
        <a href="https://twitter.com/" title="Twitter → https:&#x2F;&#x2F;twitter.com&#x2F;" rel="noopener me" target="_blank"><i class="fab fa-twitter fa-fw"></i>Twitter</a>
      </span>
  </div>

        </div>
      </div>
        <div class="back-to-top animated" role="button" aria-label="返回顶部">
          <i class="fa fa-arrow-up"></i>
          <span>0%</span>
        </div>
    </div>

    
  </aside>


    </div>

    <div class="main-inner index posts-expand">

    


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/12/12/%E7%94%B5%E8%B7%AF%E5%88%86%E6%9E%90%E5%9F%BA%E7%A1%80/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="undefined | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h2 class="post-title" itemprop="name headline">
          <a href="/blog/2023/12/12/%E7%94%B5%E8%B7%AF%E5%88%86%E6%9E%90%E5%9F%BA%E7%A1%80/" class="post-title-link" itemprop="url">电路分析基础</a>
        </h2>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-12-12 14:33:20" itemprop="dateCreated datePublished" datetime="2023-12-12T14:33:20+08:00">2023-12-12</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-12-15 17:26:57" itemprop="dateModified" datetime="2023-12-15T17:26:57+08:00">2023-12-15</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-folder"></i>
      </span>
      <span class="post-meta-item-text">分类于</span>
        <span itemprop="about" itemscope itemtype="http://schema.org/Thing">
          <a href="/blog/categories/IC%E5%9F%BA%E7%A1%80/" itemprop="url" rel="index"><span itemprop="name">IC基础</span></a>
        </span>
    </span>

  
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody">
          <h1 id="电路分析基础"><a href="#电路分析基础" class="headerlink" title="电路分析基础"></a>电路分析基础</h1><ol>
<li><p>电路： 由电器件相互连接所构成的电流通路</p>
</li>
<li><p>理想元件模型</p>
 <img src="/images/%E7%94%B5%E8%B7%AF%E5%88%86%E6%9E%90%E5%9F%BA%E7%A1%80/image-20231212143951460.png" alt="image-20231212143951460" style="zoom: 67%;" />
          <!--noindex-->
            <div class="post-button">
              <a class="btn" href="/blog/2023/12/12/%E7%94%B5%E8%B7%AF%E5%88%86%E6%9E%90%E5%9F%BA%E7%A1%80/#more" rel="contents">
                阅读全文 &raquo;
              </a>
            </div>
          <!--/noindex-->
        
      
    </div>

    
    
    

    <footer class="post-footer">
        <div class="post-eof"></div>
      
    </footer>
  </article>
</div>




    


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/11/27/Altium%20Designer/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="undefined | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h2 class="post-title" itemprop="name headline">
          <a href="/blog/2023/11/27/Altium%20Designer/" class="post-title-link" itemprop="url">未命名</a>
        </h2>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-11-27 11:00:26" itemprop="dateCreated datePublished" datetime="2023-11-27T11:00:26+08:00">2023-11-27</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-12-12 14:38:20" itemprop="dateModified" datetime="2023-12-12T14:38:20+08:00">2023-12-12</time>
    </span>

  
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody">
          <h1 id="Altium-Designer"><a href="#Altium-Designer" class="headerlink" title="Altium Designer"></a>Altium Designer</h1><ol>
<li>对于原理图元器件，Designator是唯一的，</li>
<li>原理图绘制，图形最重要，库中的元器件的值是可更改的</li>
<li>电容，即cap，NC代表什么意思？nc是纳法和皮法的缩写,它表示电容的大小非常小。具体来说,<strong>1 nc等于0.000000001F</strong></li>
<li><a target="_blank" rel="noopener" href="http://www.pcbbar.com/forum-altiumsoft-1.html">Altium</a>元器件除了“Comment”处填写参数外，如何额外添加Value值？<a target="_blank" rel="noopener" href="http://www.pcbbar.com/forum-51-1.html">altium designer</a>在原理图中默认给元器件添加的属性为“Designator”和“Comment”这两种属性，如果是绘制电阻电容这种类型器件时，可以在“Comment”栏填写“Value”值</li>
<li>贴片电容<a target="_blank" rel="noopener" href="https://item.szlcsc.com/107420.html">CC0402KRX7R9BB102</a></li>
<li>画面居中V+D</li>
<li>画三角形实心的？多边形</li>
<li>鼠标左键按住不放，鼠标呈十字状，器件为可移动状态。同时按键盘上的X或Y：X为水平左右翻转；Y为垂直上下翻转</li>
<li>按照不同的划分角度，一个器件可以被分成多个种类</li>
<li>2-2d， 3-3d，vb翻转3D图，按住键盘上的“Shift”键再用鼠标右键可以翻动板子</li>
<li>键盘上的数字键“0（英文字母上面的数字键）”可以实现PCB板的快速调整，按下数字键“9”可以实现PCB板的90度垂直翻转。】</li>
<li>m移动</li>
<li></li>
</ol>

      
    </div>

    
    
    

    <footer class="post-footer">
        <div class="post-eof"></div>
      
    </footer>
  </article>
</div>




    


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/11/01/%E5%9F%BA%E7%A1%80%E7%94%B5%E5%AD%90%E5%85%83%E5%99%A8%E4%BB%B6/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="undefined | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h2 class="post-title" itemprop="name headline">
          <a href="/blog/2023/11/01/%E5%9F%BA%E7%A1%80%E7%94%B5%E5%AD%90%E5%85%83%E5%99%A8%E4%BB%B6/" class="post-title-link" itemprop="url">基础电子元器件</a>
        </h2>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-11-01 13:59:24" itemprop="dateCreated datePublished" datetime="2023-11-01T13:59:24+08:00">2023-11-01</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-12-15 17:09:14" itemprop="dateModified" datetime="2023-12-15T17:09:14+08:00">2023-12-15</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-folder"></i>
      </span>
      <span class="post-meta-item-text">分类于</span>
        <span itemprop="about" itemscope itemtype="http://schema.org/Thing">
          <a href="/blog/categories/IC%E5%9F%BA%E7%A1%80/" itemprop="url" rel="index"><span itemprop="name">IC基础</span></a>
        </span>
    </span>

  
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody">
          <h2 id="电阻"><a href="#电阻" class="headerlink" title="电阻"></a>电阻</h2><p>电阻，即电流在电路中遇到的阻力，描述导体导电性能， 单位是Ω</p>
<p>电阻器分类有固定电阻和可变电阻，如图所示</p>
<p><img src="/blog/images/%E5%9F%BA%E7%A1%80%E7%94%B5%E5%AD%90%E5%85%83%E5%99%A8%E4%BB%B6/image-20231101141351133.png" alt="image-20231101141351133"></p>
<p>电阻在原理图的表示方法，R1-R5分别为压敏电阻，普通电阻，普通电阻，可变电阻，电位器</p>
<p><img src="/blog/images/%E5%9F%BA%E7%A1%80%E7%94%B5%E5%AD%90%E5%85%83%E5%99%A8%E4%BB%B6/image-20231101140550557.png" alt="image-20231101140550557"></p>
<p>作用：分压，限流，测温，防浪涌</p>
<p>电阻器参数：</p>
<ol>
<li>标称阻值，IEC规定了一些系列：E12(±10%) E24(±5%) E48(±2%) E192(±0.5%, ±0.25%, ±0.1%等) 。</li>
<li>允许误差，误差数值用D，F、G、J、K、M等符合表示，表明分别具有±0.5％，±1％、±2％、±5％、±10％、±20％的容许误差</li>
<li>额定功率，在规定的周围温度下，连续工作状态下可使用的最大功率。额定功率越大，体积越大。</li>
</ol>
<p>选择电阻：</p>
<ol>
<li>功能</li>
<li>主要参数：阻值，功率，精度</li>
<li>电压</li>
</ol>
          <!--noindex-->
            <div class="post-button">
              <a class="btn" href="/blog/2023/11/01/%E5%9F%BA%E7%A1%80%E7%94%B5%E5%AD%90%E5%85%83%E5%99%A8%E4%BB%B6/#more" rel="contents">
                阅读全文 &raquo;
              </a>
            </div>
          <!--/noindex-->
        
      
    </div>

    
    
    

    <footer class="post-footer">
        <div class="post-eof"></div>
      
    </footer>
  </article>
</div>




    


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/10/19/%E6%97%B6%E5%BA%8F%E5%88%86%E6%9E%90/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="undefined | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h2 class="post-title" itemprop="name headline">
          <a href="/blog/2023/10/19/%E6%97%B6%E5%BA%8F%E5%88%86%E6%9E%90/" class="post-title-link" itemprop="url">时序分析</a>
        </h2>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-10-19 15:29:09" itemprop="dateCreated datePublished" datetime="2023-10-19T15:29:09+08:00">2023-10-19</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-12-15 17:09:29" itemprop="dateModified" datetime="2023-12-15T17:09:29+08:00">2023-12-15</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-folder"></i>
      </span>
      <span class="post-meta-item-text">分类于</span>
        <span itemprop="about" itemscope itemtype="http://schema.org/Thing">
          <a href="/blog/categories/%E9%9D%99%E6%80%81%E6%97%B6%E5%BA%8F%E5%88%86%E6%9E%90/" itemprop="url" rel="index"><span itemprop="name">静态时序分析</span></a>
        </span>
    </span>

  
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody">
          <h2 id="静态时序分析原理"><a href="#静态时序分析原理" class="headerlink" title="静态时序分析原理"></a>静态时序分析原理</h2><blockquote>
<p>静态时序分析(STA),可以被定义为：对待分析的电路添加特定的时序约束，套用特定的时序模型，检验系统时序结果是否满足设计者的要求。</p>
</blockquote>
<p>静态时序分析技术是一种穷经分析方法，用以衡量电路性能。它提取整个电路所有时序路径，通过计算信号在路径上的时序传播找出违背时序约束的错误，主要是检查建立时间和保持时间是否满足要求，而他们又分别通过对最大路径时延和最小路径时延的分析得到的。</p>
<p>arrive time &#x3D; </p>
<p>{	最长路径delay累加值、</p>
<p>​          最短路径delay累加值、</p>
<p>​	路径</p>
<p>}</p>
<p>slack &#x3D; endpoint时间宽裕值</p>
          <!--noindex-->
            <div class="post-button">
              <a class="btn" href="/blog/2023/10/19/%E6%97%B6%E5%BA%8F%E5%88%86%E6%9E%90/#more" rel="contents">
                阅读全文 &raquo;
              </a>
            </div>
          <!--/noindex-->
        
      
    </div>

    
    
    

    <footer class="post-footer">
        <div class="post-eof"></div>
      
    </footer>
  </article>
</div>




    


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/09/28/EDIF/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="undefined | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h2 class="post-title" itemprop="name headline">
          <a href="/blog/2023/09/28/EDIF/" class="post-title-link" itemprop="url">EDIF</a>
        </h2>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-09-28 21:29:41" itemprop="dateCreated datePublished" datetime="2023-09-28T21:29:41+08:00">2023-09-28</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-10-18 17:36:31" itemprop="dateModified" datetime="2023-10-18T17:36:31+08:00">2023-10-18</time>
    </span>

  
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody">
          <h2 id="什么是EDIF"><a href="#什么是EDIF" class="headerlink" title="什么是EDIF"></a>什么是EDIF</h2><p>EDIF是”Electronic Design Interchange Format”的缩写，翻译为电子设计交换格式，它是一种用于描述电子设计的标准文件格式。EDIF文件通常包含了电子设计的结构、元件、连线、信号等信息，以便在不同的电子设计工具之间进行数据交换和共享。</p>
<h2 id="EDIF语句"><a href="#EDIF语句" class="headerlink" title="EDIF语句"></a>EDIF语句</h2><p>所有EDIF语句都由一个开括号、一个关键字、一些参数和一个闭括号组成。参数可以是其他语句，这就赋予了EDIF结构。实际上，一个EDIF文件只包含一条语句: <code>(edif parameters)</code></p>
<h2 id="EDIF结构"><a href="#EDIF结构" class="headerlink" title="EDIF结构"></a>EDIF结构</h2><figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br><span class="line">14</span><br><span class="line">15</span><br><span class="line">16</span><br></pre></td><td class="code"><pre><span class="line"></span><br><span class="line">(edif name</span><br><span class="line">	(status information)</span><br><span class="line">	(design where-to-find-them)</span><br><span class="line">	(external reference-libraries)</span><br><span class="line">	(library name</span><br><span class="line">		(technology defaults)</span><br><span class="line">		(cell name</span><br><span class="line">			(viewmap map)</span><br><span class="line">			(view type name</span><br><span class="line">				(interface external)</span><br><span class="line">				(contents internal)</span><br><span class="line">			)</span><br><span class="line">		)</span><br><span class="line">	)</span><br><span class="line">)</span><br></pre></td></tr></table></figure>



<p>instanceNamdef ?</p>
<p>edif用途？</p>
<p>一个元件的功能由哪些定义？即通过哪些参数就可以复刻一个元件</p>
<p>为什么不区分元件？因为线是唯一的，元件是相同的</p>
<h2 id="参考资料"><a href="#参考资料" class="headerlink" title="参考资料"></a>参考资料</h2><ol>
<li><a target="_blank" rel="noopener" href="https://www.iue.tuwien.ac.at/phd/minixhofer/node53.html">https://www.iue.tuwien.ac.at/phd/minixhofer/node53.html</a></li>
</ol>

      
    </div>

    
    
    

    <footer class="post-footer">
        <div class="post-eof"></div>
      
    </footer>
  </article>
</div>




    


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/09/15/Ocaml%EF%BC%88%E4%B8%80%EF%BC%89/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="undefined | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h2 class="post-title" itemprop="name headline">
          <a href="/blog/2023/09/15/Ocaml%EF%BC%88%E4%B8%80%EF%BC%89/" class="post-title-link" itemprop="url">Ocaml（一）</a>
        </h2>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-09-15 13:33:27" itemprop="dateCreated datePublished" datetime="2023-09-15T13:33:27+08:00">2023-09-15</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-12-15 17:08:07" itemprop="dateModified" datetime="2023-12-15T17:08:07+08:00">2023-12-15</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-folder"></i>
      </span>
      <span class="post-meta-item-text">分类于</span>
        <span itemprop="about" itemscope itemtype="http://schema.org/Thing">
          <a href="/blog/categories/OCaml/" itemprop="url" rel="index"><span itemprop="name">OCaml</span></a>
        </span>
    </span>

  
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody">
          <h2 id="1-let"><a href="#1-let" class="headerlink" title="1. let"></a>1. let</h2><blockquote>
<p>let 既不是变量声明，也不是变量赋值，而是把一个变量与不同类型的值相关联，这些关联对组成的序列称为“环境”。</p>
</blockquote>
<p>命令式语言的变量声明是给变量分配一个固定的空间，变量赋值式对这个空间的内容进行修改。</p>
<p>但是，let则是给变量动态地分配一个空间。</p>
<p>eg: </p>
<figure class="highlight ocaml"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br></pre></td><td class="code"><pre><span class="line"><span class="keyword">let</span> i = <span class="number">1</span>;;</span><br><span class="line"><span class="comment">(* val i : int = 1 *)</span></span><br><span class="line"><span class="keyword">let</span> a = <span class="number">1.2</span>;;</span><br><span class="line"><span class="comment">(* val a : float = 1.2 *)</span></span><br><span class="line"><span class="keyword">let</span> i = a;</span><br><span class="line"><span class="comment">(* val i : float = 1.2 *)</span></span><br><span class="line"></span><br><span class="line"><span class="comment">(* env = [(i, 1); (a, 1.2); (i, 1.2)]  前一个i自动失效*)</span></span><br></pre></td></tr></table></figure>

<h3 id="局部定义"><a href="#局部定义" class="headerlink" title="局部定义"></a>局部定义</h3><figure class="highlight ocaml"><table><tr><td class="gutter"><pre><span class="line">1</span><br></pre></td><td class="code"><pre><span class="line"><span class="keyword">let</span> <span class="keyword">val</span> = exp1 <span class="keyword">in</span> exp2</span><br></pre></td></tr></table></figure>

<p>注： 系统对表达式的回应以<code>-</code>开始，对定义的回应以<code>val</code>开始</p>
          <!--noindex-->
            <div class="post-button">
              <a class="btn" href="/blog/2023/09/15/Ocaml%EF%BC%88%E4%B8%80%EF%BC%89/#more" rel="contents">
                阅读全文 &raquo;
              </a>
            </div>
          <!--/noindex-->
        
      
    </div>

    
    
    

    <footer class="post-footer">
        <div class="post-eof"></div>
      
    </footer>
  </article>
</div>




    


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/09/09/Verilog-ams/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="undefined | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h2 class="post-title" itemprop="name headline">
          <a href="/blog/2023/09/09/Verilog-ams/" class="post-title-link" itemprop="url">Verilog-ams</a>
        </h2>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-09-09 16:40:35" itemprop="dateCreated datePublished" datetime="2023-09-09T16:40:35+08:00">2023-09-09</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-12-15 17:08:49" itemprop="dateModified" datetime="2023-12-15T17:08:49+08:00">2023-12-15</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-folder"></i>
      </span>
      <span class="post-meta-item-text">分类于</span>
        <span itemprop="about" itemscope itemtype="http://schema.org/Thing">
          <a href="/blog/categories/Verilog/" itemprop="url" rel="index"><span itemprop="name">Verilog</span></a>
        </span>
    </span>

  
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody">
          <h2 id="语言概述"><a href="#语言概述" class="headerlink" title="语言概述"></a>语言概述</h2><p>Verilog-AMS语言是一种高层次的模块化硬件描述语言，它用模块的形式来描述模拟系统及其子系统的结构和行为。Verilog-AMS语言可分为数字电路描述子集Verilog-HDL和模拟电路描述子集Verilog-A。</p>
<p>Verilog-AMS语言对模拟电路的描述可以分成两种类型：行为描述与结构描述。</p>
<ul>
<li>行为描述是指用一些数学表达式或者传输函数来描述目标电路的行为，其描述范围可以从基本的电阻、电容到十分复杂的滤波器或其他模拟系统；</li>
<li>结构描述则是对各个子模块在系统中 的用途以及子模块与子模块之间的连接关系进行描述，这可以理解为是对系统结构框图的描述。完整的结构描述需要包括对信号、端口和基本参数的定义。</li>
</ul>
<p><img src="/blog/../../images/Verilog-ams/image-20230910163108734.png" alt="image-20230910163108734">                                </p>
<p>Verilog-Ams的行为模为模式如下图所示：</p>
<p><img src="/blog/../../images/Verilog-ams/image-20230910165831667.png" alt="image-20230910165831667"></p>
<ul>
<li>Verilog-AMS是由模块构成的，每个模块的内容都镶嵌在<code>module</code>-<code>endmodule</code> 两个语句之间，每个模块实现特定的功能，模块可以进行层次嵌套；</li>
<li>Verilog-AMS的行为建模，关于模拟电路部分(即<strong>Verilog-A</strong>)使用的是<code>analog</code>关键字，关于数字电路部分(即<strong>Verilog</strong>)则用的是<code>always 和 initial</code>。</li>
</ul>
<p><strong>注：没有在Verilog-HDL中出现的新东西，自动认为是属于Verilog-A的部分</strong></p>
          <!--noindex-->
            <div class="post-button">
              <a class="btn" href="/blog/2023/09/09/Verilog-ams/#more" rel="contents">
                阅读全文 &raquo;
              </a>
            </div>
          <!--/noindex-->
        
      
    </div>

    
    
    

    <footer class="post-footer">
        <div class="post-eof"></div>
      
    </footer>
  </article>
</div>




    


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/09/09/Verilog/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="undefined | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h2 class="post-title" itemprop="name headline">
          <a href="/blog/2023/09/09/Verilog/" class="post-title-link" itemprop="url">Verilog</a>
        </h2>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-09-09 16:35:40" itemprop="dateCreated datePublished" datetime="2023-09-09T16:35:40+08:00">2023-09-09</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-12-15 17:24:28" itemprop="dateModified" datetime="2023-12-15T17:24:28+08:00">2023-12-15</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-folder"></i>
      </span>
      <span class="post-meta-item-text">分类于</span>
        <span itemprop="about" itemscope itemtype="http://schema.org/Thing">
          <a href="/blog/categories/Verilog/" itemprop="url" rel="index"><span itemprop="name">Verilog</span></a>
        </span>
    </span>

  
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody">
          <h2 id="Verilog"><a href="#Verilog" class="headerlink" title="Verilog"></a>Verilog</h2><h3 id="1-Verilog语言如何用于模拟电路设计的"><a href="#1-Verilog语言如何用于模拟电路设计的" class="headerlink" title="1. Verilog语言如何用于模拟电路设计的"></a>1. Verilog语言如何用于模拟电路设计的</h3><p>Verilog是一种硬件描述语言（HDL），通常用于模拟和设计数字电路。下面是使用Verilog语言进行电路设计和模拟的一般步骤：</p>
<ol>
<li><p><strong>编写Verilog代码</strong>：首先，您需要编写Verilog代码来描述您的电路。Verilog代码将包括模块定义、输入和输出端口、内部逻辑以及任何需要的组件实例化。这个代码将描述电路的结构和功能。</p>
</li>
<li><p><strong>设计层次结构</strong>：将电路分解为模块和子模块，以便更容易管理和维护代码。这有助于提高代码的可重用性和可维护性。</p>
</li>
<li><p><strong>模拟器选择</strong>：选择一个Verilog模拟器，如XSIM、ModelSim、VCS等。模拟器将用于运行Verilog代码并模拟电路的行为。</p>
</li>
<li><p><strong>创建测试台</strong>：编写测试台代码，用于提供输入信号并捕获输出信号。测试台代码通常包括测试向量生成、时钟生成以及对电路行为的监视。</p>
</li>
<li><p><strong>编译和仿真</strong>：使用Verilog模拟器编译Verilog代码并运行仿真。仿真将模拟电路的运行，并根据输入信号模拟输出信号。</p>
</li>
<li><p><strong>分析仿真结果</strong>：分析仿真输出以验证电路的正确性。检查输出是否与预期结果一致，以确保电路按照设计规范工作。</p>
</li>
<li><p><strong>优化和修改</strong>：根据仿真结果，对Verilog代码进行优化或修改，以改进电路性能或修复问题。</p>
</li>
<li><p><strong>重复测试</strong>：重复上述步骤，直到满足设计规范和性能要求。</p>
</li>
<li><p><strong>综合和实际实现</strong>：一旦满足了设计规范，可以将Verilog代码综合成门级电路，并使用工具如Xilinx Vivado、Synopsys Design Compiler等将其映射到FPGA或ASIC。</p>
</li>
<li><p><strong>验证硬件</strong>：在实际硬件上验证电路，确保它在实际环境中正常工作。</p>
</li>
</ol>
<p>总之，Verilog语言是一种强大的工具，用于模拟和设计数字电路。通过编写Verilog代码并使用仿真器，您可以有效地验证电路的功能和性能，然后将其实现在硬件中。这个过程通常在数字电路设计中扮演着关键的角色。</p>
          <!--noindex-->
            <div class="post-button">
              <a class="btn" href="/blog/2023/09/09/Verilog/#more" rel="contents">
                阅读全文 &raquo;
              </a>
            </div>
          <!--/noindex-->
        
      
    </div>

    
    
    

    <footer class="post-footer">
        <div class="post-eof"></div>
      
    </footer>
  </article>
</div>




    


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/07/22/SF-1-Logic/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="undefined | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h2 class="post-title" itemprop="name headline">
          <a href="/blog/2023/07/22/SF-1-Logic/" class="post-title-link" itemprop="url">SF-1-Logic</a>
        </h2>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-07-22 10:43:43" itemprop="dateCreated datePublished" datetime="2023-07-22T10:43:43+08:00">2023-07-22</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-12-15 17:08:34" itemprop="dateModified" datetime="2023-12-15T17:08:34+08:00">2023-12-15</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-folder"></i>
      </span>
      <span class="post-meta-item-text">分类于</span>
        <span itemprop="about" itemscope itemtype="http://schema.org/Thing">
          <a href="/blog/categories/Coq/" itemprop="url" rel="index"><span itemprop="name">Coq</span></a>
        </span>
    </span>

  
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody">
          <h2 id="前言"><a href="#前言" class="headerlink" title="前言"></a>前言</h2><p>在前面的学习中，我们证明了大量的命题：*’相等性命题’*（e1 &#x3D; e2）、蕴含式（P → Q）和量化命题 （∀ x, P x），在本章中，我们将会看到如何用 Coq 解决类似形式的逻辑推理。</p>
<p>对于*命题(Prop)*，有这如下的特点：</p>
<ul>
<li><p>所有语法形式良好的命题，无论是否为真，其类型均为 Prop</p>
</li>
<li><p>命题还是*’一等的（First-Class）’*实体， 即在 Coq 的世界中，我们可以像操作其它实体那样操作命题</p>
</li>
<li><p>命题可既以出现在 Theorem（还有 Lemma 以及 Example）的声明中，也可以用 Definition 为命题取名，之后我们可以在任何需要此命题的地方使用它们名字</p>
</li>
<li><p>*’参数化’*的命题 – 也就是一个接受某些类型的参数， 然后返回一个命题的函数</p>
          <!--noindex-->
            <div class="post-button">
              <a class="btn" href="/blog/2023/07/22/SF-1-Logic/#more" rel="contents">
                阅读全文 &raquo;
              </a>
            </div>
          <!--/noindex-->
        
      
    </div>

    
    
    

    <footer class="post-footer">
        <div class="post-eof"></div>
      
    </footer>
  </article>
</div>




    


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/07/19/SF-1-Tactics/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="undefined | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h2 class="post-title" itemprop="name headline">
          <a href="/blog/2023/07/19/SF-1-Tactics/" class="post-title-link" itemprop="url">SF-1-Tactics</a>
        </h2>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-07-19 17:19:31" itemprop="dateCreated datePublished" datetime="2023-07-19T17:19:31+08:00">2023-07-19</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-12-15 17:08:43" itemprop="dateModified" datetime="2023-12-15T17:08:43+08:00">2023-12-15</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-folder"></i>
      </span>
      <span class="post-meta-item-text">分类于</span>
        <span itemprop="about" itemscope itemtype="http://schema.org/Thing">
          <a href="/blog/categories/Coq/" itemprop="url" rel="index"><span itemprop="name">Coq</span></a>
        </span>
    </span>

  
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody">
          <h2 id="apply策略"><a href="#apply策略" class="headerlink" title="apply策略"></a>apply策略</h2><p>当遇到如下场景时，采用apply策略：</p>
<ul>
<li><p>待证目标与上下文中的前提或已证引理*’刚好相同’*的情况</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br></pre></td><td class="code"><pre><span class="line">Theorem silly1 : forall (n m : nat),</span><br><span class="line">  n = m -&gt; n = m.</span><br><span class="line">Proof. intros n m eq. apply eq.  Qed.</span><br></pre></td></tr></table></figure>
</li>
<li><p>待证目标存在于一个蕴含式中，就可以配合*’条件（Conditional）’*假设和引理来使用，该蕴含式的前提就会被添加到待证子目标列表中</p>
</li>
<li><p>当我们使用 apply H 时，语句 H 会以一个引入了某些 <em>‘通用变量（Universal Variables）’</em> 的 ∀ 开始。在 Coq 针对 H 的结论匹配当前目标时，它会尝试为这些变量查找适当的值</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br></pre></td><td class="code"><pre><span class="line">Theorem silly2a : forall (n m : nat),</span><br><span class="line">  (n,n) = (m,m)  -&gt;</span><br><span class="line">  (forall (q r : nat), (q,q) = (r,r) -&gt; [q] = [r]) -&gt;</span><br><span class="line">  [n] = [m].</span><br><span class="line">Proof.</span><br><span class="line">  intros n m eq1 eq2.</span><br><span class="line">  apply eq2. apply eq1.  Qed.</span><br><span class="line"></span><br></pre></td></tr></table></figure>

<p>变量 q 匹配n ，而 r 匹配m </p>
</li>
<li><p>要使用 apply 策略，被应用的事实（的结论）必须精确地匹配证明目标： 例如, 当等式的左右两边互换后，apply 就无法起效了，这个时候需要采用<strong>symmetry</strong></p>
</li>
</ul>
          <!--noindex-->
            <div class="post-button">
              <a class="btn" href="/blog/2023/07/19/SF-1-Tactics/#more" rel="contents">
                阅读全文 &raquo;
              </a>
            </div>
          <!--/noindex-->
        
      
    </div>

    
    
    

    <footer class="post-footer">
        <div class="post-eof"></div>
      
    </footer>
  </article>
</div>




  <nav class="pagination">
    <span class="page-number current">1</span><a class="page-number" href="/blog/page/2/">2</a><a class="page-number" href="/blog/page/3/">3</a><a class="extend next" rel="next" title="下一页" aria-label="下一页" href="/blog/page/2/"><i class="fa fa-angle-right"></i></a>
  </nav>

</div>
  </main>

  <footer class="footer">
    <div class="footer-inner">


<div class="copyright">
  &copy; 
  <span itemprop="copyrightYear">2023</span>
  <span class="with-love">
    <i class="fa fa-heart"></i>
  </span>
  <span class="author" itemprop="copyrightHolder">yanlw</span>
</div>
<div class="busuanzi-count">
    <span class="post-meta-item" id="busuanzi_container_site_uv">
      <span class="post-meta-item-icon">
        <i class="fa fa-user"></i>
      </span>
      <span class="site-uv" title="总访客量">
        <span id="busuanzi_value_site_uv"></span>
      </span>
    </span>
    <span class="post-meta-item" id="busuanzi_container_site_pv">
      <span class="post-meta-item-icon">
        <i class="fa fa-eye"></i>
      </span>
      <span class="site-pv" title="总访问量">
        <span id="busuanzi_value_site_pv"></span>
      </span>
    </span>
</div>
  <div class="powered-by">由 <a href="https://hexo.io/" rel="noopener" target="_blank">Hexo</a> & <a href="https://theme-next.js.org/pisces/" rel="noopener" target="_blank">NexT.Pisces</a> 强力驱动
  </div>

    </div>
  </footer>

  
  <div class="reading-progress-bar"></div>

  <a href="https://gitee.com/yanlwsometing" class="github-corner" title="在 GitHub 上关注我" aria-label="在 GitHub 上关注我" rel="noopener" target="_blank"><svg width="80" height="80" viewBox="0 0 250 250" aria-hidden="true"><path d="M0,0 L115,115 L130,115 L142,142 L250,250 L250,0 Z"></path><path d="M128.3,109.0 C113.8,99.7 119.0,89.6 119.0,89.6 C122.0,82.7 120.5,78.6 120.5,78.6 C119.2,72.0 123.4,76.3 123.4,76.3 C127.3,80.9 125.5,87.3 125.5,87.3 C122.9,97.6 130.6,101.9 134.4,103.2" fill="currentColor" style="transform-origin: 130px 106px;" class="octo-arm"></path><path d="M115.0,115.0 C114.9,115.1 118.7,116.5 119.8,115.4 L133.7,101.6 C136.9,99.2 139.9,98.4 142.2,98.6 C133.8,88.0 127.5,74.4 143.8,58.0 C148.5,53.4 154.0,51.2 159.7,51.0 C160.3,49.4 163.2,43.6 171.4,40.1 C171.4,40.1 176.1,42.5 178.8,56.2 C183.1,58.6 187.2,61.8 190.9,65.4 C194.5,69.0 197.7,73.2 200.1,77.6 C213.8,80.2 216.3,84.9 216.3,84.9 C212.7,93.1 206.9,96.0 205.4,96.6 C205.1,102.4 203.0,107.8 198.3,112.5 C181.9,128.9 168.3,122.5 157.7,114.1 C157.9,116.9 156.7,120.9 152.7,124.9 L141.0,136.5 C139.8,137.7 141.6,141.9 141.8,141.8 Z" fill="currentColor" class="octo-body"></path></svg></a>

<noscript>
  <div class="noscript-warning">Theme NexT works best with JavaScript enabled</div>
</noscript>


  
  <script src="https://cdnjs.cloudflare.com/ajax/libs/animejs/3.2.1/anime.min.js" integrity="sha256-XL2inqUJaslATFnHdJOi9GfQ60on8Wx1C2H8DYiN1xY=" crossorigin="anonymous"></script>
  <script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.6.4/jquery.min.js" integrity="sha256-oP6HI9z1XaZNBrJURtCoUT5SUnxFr8s3BzRl+cbzUq8=" crossorigin="anonymous"></script>
  <script src="https://cdnjs.cloudflare.com/ajax/libs/fancybox/3.5.7/jquery.fancybox.min.js" integrity="sha256-yt2kYMy0w8AbtF89WXb2P1rfjcP/HTHLT7097U8Y5b8=" crossorigin="anonymous"></script>
<script src="/blog/js/comments.js"></script><script src="/blog/js/utils.js"></script><script src="/blog/js/next-boot.js"></script>

  


  <script src="/blog/js/third-party/fancybox.js"></script>



  
  <script async src="https://busuanzi.ibruce.info/busuanzi/2.3/busuanzi.pure.mini.js"></script>





</body>
</html>
